\begin{tabbing}
$\forall$\=$i$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $A$:ecl(${\it ds}$;${\it da}$), ${\it snd}$:msg{-}spec(${\it ds}$;${\it da}$),\+
\\[0ex]${\it upd}$:update{-}spec(${\it ds}$;${\it da}$), $j$:Id.
\-\\[0ex]msg{-}spec{-}loc(${\it snd}$;$i$)
\\[0ex]$\Rightarrow$ (\=R{-}has{-}loc(\=ecl{-}machine at $i$ with state ecl\+\+
\\[0ex]
\\[0ex]$A$
\\[0ex]
\\[0ex]state variables ${\it ds}$
\\[0ex]
\\[0ex]actions ${\it da}$
\\[0ex]
\\[0ex]sends ${\it snd}$
\\[0ex]
\\[0ex]updates ${\it upd}$;$j$)
\-\\[0ex]$\sim$
\\[0ex]$i$ = $j$)
\-
\end{tabbing}